The formulae-as-types notion of construction